\begin{tabbing}
$\forall$$A$, $B$:Realizer.
\\[0ex]R{-}interface($A$;$B$)
\\[0ex]$\Leftrightarrow$
\\[0ex](\=$\forall$$i$:Id.\+
\\[0ex]R{-}has{-}loc($B$;$i$)
\\[0ex]$\Rightarrow$ \=$\forall$$k$$\in$dom(R{-}da($B$;$i$)). \+
\\[0ex]
\\[0ex]$T$\==R{-}da($B$;$i$)($k$) $\Rightarrow$ \+
\\[0ex]isrcv($k$) $\Rightarrow$ destination(lnk($k$)) $=$ $i$ $\in$ Id $\Rightarrow$ R{-}da($A$;source(lnk($k$)))($k$)?Void $\subseteq\rho$ $T$)
\-\-\-
\end{tabbing}